Inference at * 
Iof proof for Lemma member-exists:


  T:Type, L:(T List). (x:T. (x  L))  ((L = [])) 

latex

 by MaAuto 

latex

 1: 

 1: 1. T : Type
 1: 2. L : T List
 1: 3. x:T. (x  L)
 1:   (L = [])
 2: 

 2: 1. T : Type
 2: 2. L : T List
 2: 3. (L = [])
 2:   x:T. (x  L)
 .

Definitions	P  Q, P & Q, a < b, P  Q, (x  l), , False, P  Q, Void, x:A. B(x), x:A  B(x), A, x:A. B(x), x:AB(x), , [], type List, s = t, t  T, Type
Lemmas	iff wf, false wf, rev implies wf, l member wf, not wf